(* SPDX-License-Identifier: GPL-2.0 or GPL-3.0
   Copyright © 2019 Ariadne Devos *)

Require Import Coq.Lists.List.
Require Import Coq.omega.Omega.

(* Vector bounds *)

(* Less than a constant,
   e.g. less than UINT8_MAX or SIZE_MAX *)
Definition vector_lt_constant (up : nat) : list nat -> Prop
  := List.Forall (gt up).

(* E.g., less-than the radix -> fits in machine type *)
Theorem vector_lt_constant_lift (x : nat) (y : nat) (p : x <= y) : forall t, vector_lt_constant x t -> vector_lt_constant y t.
Proof.
  intro t.
  unfold vector_lt_constant.
  apply Forall_impl.
  intro a.
  omega.
Qed.

Theorem vector_lt_constant_vacuous x : vector_lt_constant x nil.
Proof. apply Forall_nil. Qed.

Theorem vector_lt_peell x a v' : vector_lt_constant x (a :: v') <-> x > a /\ vector_lt_constant x v'.
Proof.
  unfold vector_lt_constant.
  intuition.
  + apply (Forall_inv H).
  + inversion H.
    assumption.
Qed.
